$\forall$${\it es}$:ES, $A$, $T$:Type, $X$:AbsInterface($A$), ${\it base}$:$T$, $f$:($T$$\rightarrow$$A$$\rightarrow$$T$), $e$:E.
\\[0ex]prior{-}state($f$;${\it base}$;$X$;$e$) $\in$ $T$